Defines predicate saying that a binary relation over some type
is well-founded.
Well-foundedness is phrased in terms of a `course of values'
induction principle, since this is more useful constructively
than alternative formulations (e.g. saying that there are
no infinite descending chains, or saying that every non-empty
subset has a minimal element). NB: constructively, these
alternative formulations are not equivalent.
Lemmas and tactics are introduced for induction on the rank of
an expression (`inverse image induction'). One deficiency of Nuprl's
type theory is that in some situations (notably when proving well-formedness
goals) lemmas are unusable, and instead one must resort to using
tactics that reproduce equivalent sequences of primitive rules.
The theorem `inv_image_ind_tp' provides a template for such a tactic
that mirrors the `inv_image_ind_a' lemma.